COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	top[e86,jmc]	An object can't be on top of itself
C00008 ENDMK
C⊗;
top[e86,jmc]	An object can't be on top of itself

	The fact that an object can't be put on top its own top
is included in the blocks world axioms of (McCarthy 1986) as
an afterthought; previous axioms omitted the restriction.
The consequence of omitting the restriction is that putting
an object on top of itself would be allowed, but it could not
subsequently be moved, because it wouldn't be clear.  Problem
solvers might be distracted into wasting a little time by the
omission, but it's hard to say what harm could be done unless
one could imagine a goal that would allow a block being on
itself as a spurious solution.  It's different when we are
trying to model correctness, since it is indeed impossible for
a block to be on top of itself.

	We may include as an axiom the fact that in no situation
is a block on top of itself or, more generally, above itself,
where the $above$ relation is the transitive closure of $on$.
If we use an ordinary monotonic logic and the usual blocks axioms
about moving, this makes the axiom set contradictory, since a
possible action results in an impossible situation.  Actually to
get a contradiction we need the existence of at least one situation
with a movable block.  If our axioms for moving blocks contain
a non-abnormality premiss, which assumes circumscription will
be used, then they remain consistent when
we add the fact that a block cannot be above itself.
We merely conclude something like $ab\ aspect2(x,move(x,top\ x),s)$.

	However, and this is the main point of this note, there
is another desirable property of sets of situation calculus axioms
which is lost.  Namely, it should be possible to determine what actions
are possible in a given situation by considering only the facts about
that situation, i.e. it shouldn't be necessary to reason about the future
or the past.  We may conjecture that one reason why ordinary general
purpose theorem provers sometimes encounter combinatorial explosion
in reasoning about the blocks world is that the theorem prover may
generate large numbers of terms like $result(e3,result(e2,result(e1,s)))$
which are irrelevant to determining what actions are possible in a given
situation.  STRIPS avoids this, since it does predicate calculus reasoning
only within a situation.  As I have remarked elsewhere, we should learn
from this, the need for controllable theorem provers --- e.g. we should
be able to tell the theorem prover to limit its substitutions to a
given situation in determining what actions are possible in the situation.

	This desirable property is lost if we must reason about a future
situation being impossible in order to determine that moving a block
to its own top is impossible.  Therefore, I think we should imagine
an intelligent program proceeding as follows.  It begins with
an abnormality theory like that of (McCarthy 1986), probably modified
to use Lifschitz's pointwise circumscription as proposed in his (1986).
From this it deduces that an object cannot be moved to its own top as
a general proposition.  It does this because it wants a system in which
what can be done in a situation is determined entirely by what fluents
(McCarthy and Hayes 1969) apply in that situation.

Remark: Such restrictions on what can be substituted amount to going to
a sorted logic, e.g. we imagine replacing the variable $s$ in
certain formulas by a variable $s1$ restricted to a certain sort.
The sorts won't be those usually chosen, e.g. we may sometimes
have a formula $∀s1.s1=S0$, and this imposes the restriction
that we only consider substituting $S0$ for $s$ in this formula.
We are interested in metatheorems that certain kinds of formulas
are provable in the original theory iff they are provable in the
theory that has been weakened in this manner.